T:Type, L:(T List).
(0 < ||L||)  no_repeats(T;L)  (a:T. adjacent(T;L;last(L);a)  False) 

latex

Definitions	t  T, type List, s = t, Type, x:AB(x), a < b, no_repeats(T;l), adjacent(T;L;x;y), False, P  Q, x:A. B(x), P  Q, P & Q, x:A  B(x), P  Q, last(L), A, b, [], , #$n, l[i], i z j, i <z j, hd(l), [car / cdr], ||as||, Void, n+m, A List, True, T, left + right, P  Q, i  j , A  B, , , {x:A| B(x)} , n - m, s ~ t
Lemmas	no repeats cons, select cons tl, nat wf, member wf, le wf, length cons, non neg length, adjacent-cons, rev implies wf, squash wf, true wf, last cons, length wf1, adjacent-singleton, not wf, assert wf, last wf, false wf, adjacent wf, iff wf, no repeats wf